Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    minus(x,0)  → x
2:    minus(s(x),s(y))  → minus(x,y)
3:    double(0)  → 0
4:    double(s(x))  → s(s(double(x)))
5:    plus(0,y)  → y
6:    plus(s(x),y)  → s(plus(x,y))
7:    plus(s(x),y)  → plus(x,s(y))
8:    plus(s(x),y)  → s(plus(minus(x,y),double(y)))
9:    plus(s(plus(x,y)),z)  → s(plus(plus(x,y),z))
There are 8 dependency pairs:
10:    MINUS(s(x),s(y))  → MINUS(x,y)
11:    DOUBLE(s(x))  → DOUBLE(x)
12:    PLUS(s(x),y)  → PLUS(x,y)
13:    PLUS(s(x),y)  → PLUS(x,s(y))
14:    PLUS(s(x),y)  → PLUS(minus(x,y),double(y))
15:    PLUS(s(x),y)  → MINUS(x,y)
16:    PLUS(s(x),y)  → DOUBLE(y)
17:    PLUS(s(plus(x,y)),z)  → PLUS(plus(x,y),z)
The approximated dependency graph contains 3 SCCs: {11}, {10} and {12-14,17}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.05 seconds)   ---  May 4, 2006